A function prototype documents the interface to a function. It serves as a contract between the function and its caller. In early versions of C, the function "prototype" was very limited. It described the type returned by the function but nothing about its parameters. The main improvement provided by ANSI C was the ability to add information on the number and types of parameter to a function. LCLint provides the means to express much more about a function interface: what global variable the function may use, what values visible to the caller it may modify, if a pointer parameter may be a null pointer or point to undefined storage, if storage pointed to by a parameter is deallocated before the function returns, if the function may create new aliases to a parameter, can the caller modify or deallocate the return value, etc.
The extra interface information places constraints on both how the function may be called and how it may be implemented. LCLint reports places where these constrains are not satisfied. Typically, these indicate bugs in the code or errors in the interface documentation.
This section describes syntactic comments may be added to a function declaration to document what global variables the function implementation may use and what values visible to its caller it may modify. Sections 5-7 describe annotations may be added to parameters to constrain valid arguments to a function and how these arguments may be used after the call and to the return value to constrain results.
int f (int *p, int *q) /*@modifies *p@*/;declares a function f that may modify the value pointed to by its first argument but may not modify the value of its second argument or any global state.
LCLint checks that a function does not modify any caller-visible value not encompassed by its modifies clause and does modify all values listed in its modifies clause on some possible execution of the function. Figure 4 shows an example of modifies checking done by LCLint.
internalState
The function modifies some internal state (that is, the value of a static variable). Even though a client cannot access the internal state directly, it is important to know that something may be modified by the function call both for clear documentation and for checking undefined order of evaluation (Section 10.1) and side-effect free parameters (Section 8.2.1).fileSystem
The function modifies the file system. Any modification that may change the system state is considered a file system modification. All functions that modify an object of type pointer to FILE also modify the file system. In addition, functions that do not modify a FILE pointer but modify some state that is visible outside this process also modify the file system (e.g., rename). The flag mod-file-system controls reporting of undocumented file system modifications.nothing
The function modifies nothing (i.e., it is side-effect free).
The syntactic comment, /*@*/ in a function declaration or definition (after the parameter list, before the semi-colon or function body) denotes a function that modifies nothing and does not use any global variables (see Section 4.2).
A function with no modifies clause is an unconstrained function since there are no documented constraints on what it may modify. When an unconstrained function is called, it is checked differently from a function declared with a modifies clause. To prevent spurious errors, no modification error is reported at the call site unless the moduncon flag is on. Flags control whether errors involving unconstrained functions are reported for other checks that depend on modifications (side-effect free macro parameters (Section 8.2.1), undefined evaluation order (Section 10.1), and likely infinite loops (Section 10.2.1).)
Figure 5 shows an example function definition with a globals list and associated checking done by LCLint.
A global or file static variable declaration may be preceded by an annotation to indicate how the variable should be checked. In order of decreasing checks, the annotations are:
/*@checkedstrict@*/
Strictest checking. Undocumented uses and modifications of the variable are reported in all functions whether or not they have a globals list (unless checkstrictglobs is off)./*@checked@*/
Undocumented use of the variable is reported in a function with a globals list, but not in a function declared with no globals (unless globnoglobs is on)./*@checkmod@*/
Undocumented uses of the variable are not reported, but undocumented modifications are reported. (If modglobsnomods is on, errors are reported even in functions declared with no modifies clause or globals list.)/*@unchecked@*/
No messages are reported for undocumented use or modification of this global variable. If a variable has none of these annotations, an implicit annotation is determined by the flag settings.
Different flags control the implicit annotation for variables declared with global scope and variables declared with file scope (i.e., using the static storage qualifier). To set the implicit annotation for global variables declared in context (globs for external variables or statics for file static variable) to be annotation (checked, checkmod, checkedstrict) use imp<annotation><context>. For example, +impcheckedstrictstatics makes the implicit checking on unqualified file static variables checkedstrict. (See Apppendix C, page 51, for a complete list of globals checking flags.)
Later declarations may not include variables in the globals list that were not included in the first declaration. The exception to this is when the first declaration is in a header file and the later declaration or definition includes file static variables. Since these are not visible in the header file, they can not be included in the header file declaration. Similarly, the modifies clause of a later declaration may not include objects that are not modifiable in the first declaration. The later declaration may be more specific. For example, if the header declaration is:
extern void setName (employee e, char *s) /*@modifies e@*/;the later declaration could be,
void setName (employee e, char *) /*@modifies e->name@*/;If employee is an abstract type, the declaration in the header should not refer to a particular implementation (i.e., it shouldn't rely on there being a name field), but the implementation declaration can be more specific.
This rule also applies to file static variables. The header declaration for a function that modifies a file static variable should use modifies internalState since file static variables are not visible to clients. The implementation declaration should list the actual file static variables that may be modified.
